WORST_CASE(?,O(n^3))
* Step 1: DependencyPairs WORST_CASE(?,O(n^3))
+ Considered Problem:
- Strict TRS:
append(dd(x,xs),ys) -> dd(x,append(xs,ys))
append(nil(),ys) -> ys
gt(0(),0()) -> false()
gt(0(),s(y)) -> false()
gt(s(x),0()) -> true()
gt(s(x),s(y)) -> gt(x,y)
quicksort(dd(z,zs)) -> quicksort'(z,split(z,zs))
quicksort(nil()) -> nil()
quicksort'(z,pair(xs,ys)) -> append(quicksort(xs),dd(z,quicksort(ys)))
split(pivot,dd(x,xs)) -> split'(gt(x,pivot),x,split(pivot,xs))
split(pivot,nil()) -> pair(nil(),nil())
split'(false(),x,pair(ls,rs)) -> pair(dd(x,ls),rs)
split'(true(),x,pair(ls,rs)) -> pair(ls,dd(x,rs))
- Signature:
{append/2,gt/2,quicksort/1,quicksort'/2,split/2,split'/3} / {0/0,dd/2,false/0,nil/0,pair/2,s/1,true/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {append,gt,quicksort,quicksort',split
,split'} and constructors {0,dd,false,nil,pair,s,true}
+ Applied Processor:
DependencyPairs {dpKind_ = DT}
+ Details:
We add the following dependency tuples:
Strict DPs
append#(dd(x,xs),ys) -> c_1(append#(xs,ys))
append#(nil(),ys) -> c_2()
gt#(0(),0()) -> c_3()
gt#(0(),s(y)) -> c_4()
gt#(s(x),0()) -> c_5()
gt#(s(x),s(y)) -> c_6(gt#(x,y))
quicksort#(dd(z,zs)) -> c_7(quicksort'#(z,split(z,zs)),split#(z,zs))
quicksort#(nil()) -> c_8()
quicksort'#(z,pair(xs,ys)) -> c_9(append#(quicksort(xs),dd(z,quicksort(ys))),quicksort#(xs),quicksort#(ys))
split#(pivot,dd(x,xs)) -> c_10(split'#(gt(x,pivot),x,split(pivot,xs)),gt#(x,pivot),split#(pivot,xs))
split#(pivot,nil()) -> c_11()
split'#(false(),x,pair(ls,rs)) -> c_12()
split'#(true(),x,pair(ls,rs)) -> c_13()
Weak DPs
and mark the set of starting terms.
* Step 2: PredecessorEstimation WORST_CASE(?,O(n^3))
+ Considered Problem:
- Strict DPs:
append#(dd(x,xs),ys) -> c_1(append#(xs,ys))
append#(nil(),ys) -> c_2()
gt#(0(),0()) -> c_3()
gt#(0(),s(y)) -> c_4()
gt#(s(x),0()) -> c_5()
gt#(s(x),s(y)) -> c_6(gt#(x,y))
quicksort#(dd(z,zs)) -> c_7(quicksort'#(z,split(z,zs)),split#(z,zs))
quicksort#(nil()) -> c_8()
quicksort'#(z,pair(xs,ys)) -> c_9(append#(quicksort(xs),dd(z,quicksort(ys))),quicksort#(xs),quicksort#(ys))
split#(pivot,dd(x,xs)) -> c_10(split'#(gt(x,pivot),x,split(pivot,xs)),gt#(x,pivot),split#(pivot,xs))
split#(pivot,nil()) -> c_11()
split'#(false(),x,pair(ls,rs)) -> c_12()
split'#(true(),x,pair(ls,rs)) -> c_13()
- Weak TRS:
append(dd(x,xs),ys) -> dd(x,append(xs,ys))
append(nil(),ys) -> ys
gt(0(),0()) -> false()
gt(0(),s(y)) -> false()
gt(s(x),0()) -> true()
gt(s(x),s(y)) -> gt(x,y)
quicksort(dd(z,zs)) -> quicksort'(z,split(z,zs))
quicksort(nil()) -> nil()
quicksort'(z,pair(xs,ys)) -> append(quicksort(xs),dd(z,quicksort(ys)))
split(pivot,dd(x,xs)) -> split'(gt(x,pivot),x,split(pivot,xs))
split(pivot,nil()) -> pair(nil(),nil())
split'(false(),x,pair(ls,rs)) -> pair(dd(x,ls),rs)
split'(true(),x,pair(ls,rs)) -> pair(ls,dd(x,rs))
- Signature:
{append/2,gt/2,quicksort/1,quicksort'/2,split/2,split'/3,append#/2,gt#/2,quicksort#/1,quicksort'#/2,split#/2
,split'#/3} / {0/0,dd/2,false/0,nil/0,pair/2,s/1,true/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/2,c_8/0
,c_9/3,c_10/3,c_11/0,c_12/0,c_13/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {append#,gt#,quicksort#,quicksort'#,split#
,split'#} and constructors {0,dd,false,nil,pair,s,true}
+ Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
+ Details:
We estimate the number of application of
{2,3,4,5,8,11,12,13}
by application of
Pre({2,3,4,5,8,11,12,13}) = {1,6,7,9,10}.
Here rules are labelled as follows:
1: append#(dd(x,xs),ys) -> c_1(append#(xs,ys))
2: append#(nil(),ys) -> c_2()
3: gt#(0(),0()) -> c_3()
4: gt#(0(),s(y)) -> c_4()
5: gt#(s(x),0()) -> c_5()
6: gt#(s(x),s(y)) -> c_6(gt#(x,y))
7: quicksort#(dd(z,zs)) -> c_7(quicksort'#(z,split(z,zs)),split#(z,zs))
8: quicksort#(nil()) -> c_8()
9: quicksort'#(z,pair(xs,ys)) -> c_9(append#(quicksort(xs),dd(z,quicksort(ys)))
,quicksort#(xs)
,quicksort#(ys))
10: split#(pivot,dd(x,xs)) -> c_10(split'#(gt(x,pivot),x,split(pivot,xs)),gt#(x,pivot),split#(pivot,xs))
11: split#(pivot,nil()) -> c_11()
12: split'#(false(),x,pair(ls,rs)) -> c_12()
13: split'#(true(),x,pair(ls,rs)) -> c_13()
* Step 3: RemoveWeakSuffixes WORST_CASE(?,O(n^3))
+ Considered Problem:
- Strict DPs:
append#(dd(x,xs),ys) -> c_1(append#(xs,ys))
gt#(s(x),s(y)) -> c_6(gt#(x,y))
quicksort#(dd(z,zs)) -> c_7(quicksort'#(z,split(z,zs)),split#(z,zs))
quicksort'#(z,pair(xs,ys)) -> c_9(append#(quicksort(xs),dd(z,quicksort(ys))),quicksort#(xs),quicksort#(ys))
split#(pivot,dd(x,xs)) -> c_10(split'#(gt(x,pivot),x,split(pivot,xs)),gt#(x,pivot),split#(pivot,xs))
- Weak DPs:
append#(nil(),ys) -> c_2()
gt#(0(),0()) -> c_3()
gt#(0(),s(y)) -> c_4()
gt#(s(x),0()) -> c_5()
quicksort#(nil()) -> c_8()
split#(pivot,nil()) -> c_11()
split'#(false(),x,pair(ls,rs)) -> c_12()
split'#(true(),x,pair(ls,rs)) -> c_13()
- Weak TRS:
append(dd(x,xs),ys) -> dd(x,append(xs,ys))
append(nil(),ys) -> ys
gt(0(),0()) -> false()
gt(0(),s(y)) -> false()
gt(s(x),0()) -> true()
gt(s(x),s(y)) -> gt(x,y)
quicksort(dd(z,zs)) -> quicksort'(z,split(z,zs))
quicksort(nil()) -> nil()
quicksort'(z,pair(xs,ys)) -> append(quicksort(xs),dd(z,quicksort(ys)))
split(pivot,dd(x,xs)) -> split'(gt(x,pivot),x,split(pivot,xs))
split(pivot,nil()) -> pair(nil(),nil())
split'(false(),x,pair(ls,rs)) -> pair(dd(x,ls),rs)
split'(true(),x,pair(ls,rs)) -> pair(ls,dd(x,rs))
- Signature:
{append/2,gt/2,quicksort/1,quicksort'/2,split/2,split'/3,append#/2,gt#/2,quicksort#/1,quicksort'#/2,split#/2
,split'#/3} / {0/0,dd/2,false/0,nil/0,pair/2,s/1,true/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/2,c_8/0
,c_9/3,c_10/3,c_11/0,c_12/0,c_13/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {append#,gt#,quicksort#,quicksort'#,split#
,split'#} and constructors {0,dd,false,nil,pair,s,true}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:S:append#(dd(x,xs),ys) -> c_1(append#(xs,ys))
-->_1 append#(nil(),ys) -> c_2():6
-->_1 append#(dd(x,xs),ys) -> c_1(append#(xs,ys)):1
2:S:gt#(s(x),s(y)) -> c_6(gt#(x,y))
-->_1 gt#(s(x),0()) -> c_5():9
-->_1 gt#(0(),s(y)) -> c_4():8
-->_1 gt#(0(),0()) -> c_3():7
-->_1 gt#(s(x),s(y)) -> c_6(gt#(x,y)):2
3:S:quicksort#(dd(z,zs)) -> c_7(quicksort'#(z,split(z,zs)),split#(z,zs))
-->_2 split#(pivot,dd(x,xs)) -> c_10(split'#(gt(x,pivot),x,split(pivot,xs))
,gt#(x,pivot)
,split#(pivot,xs)):5
-->_1 quicksort'#(z,pair(xs,ys)) -> c_9(append#(quicksort(xs),dd(z,quicksort(ys)))
,quicksort#(xs)
,quicksort#(ys)):4
-->_2 split#(pivot,nil()) -> c_11():11
4:S:quicksort'#(z,pair(xs,ys)) -> c_9(append#(quicksort(xs),dd(z,quicksort(ys)))
,quicksort#(xs)
,quicksort#(ys))
-->_3 quicksort#(nil()) -> c_8():10
-->_2 quicksort#(nil()) -> c_8():10
-->_1 append#(nil(),ys) -> c_2():6
-->_3 quicksort#(dd(z,zs)) -> c_7(quicksort'#(z,split(z,zs)),split#(z,zs)):3
-->_2 quicksort#(dd(z,zs)) -> c_7(quicksort'#(z,split(z,zs)),split#(z,zs)):3
-->_1 append#(dd(x,xs),ys) -> c_1(append#(xs,ys)):1
5:S:split#(pivot,dd(x,xs)) -> c_10(split'#(gt(x,pivot),x,split(pivot,xs)),gt#(x,pivot),split#(pivot,xs))
-->_1 split'#(true(),x,pair(ls,rs)) -> c_13():13
-->_1 split'#(false(),x,pair(ls,rs)) -> c_12():12
-->_3 split#(pivot,nil()) -> c_11():11
-->_2 gt#(s(x),0()) -> c_5():9
-->_2 gt#(0(),s(y)) -> c_4():8
-->_2 gt#(0(),0()) -> c_3():7
-->_3 split#(pivot,dd(x,xs)) -> c_10(split'#(gt(x,pivot),x,split(pivot,xs))
,gt#(x,pivot)
,split#(pivot,xs)):5
-->_2 gt#(s(x),s(y)) -> c_6(gt#(x,y)):2
6:W:append#(nil(),ys) -> c_2()
7:W:gt#(0(),0()) -> c_3()
8:W:gt#(0(),s(y)) -> c_4()
9:W:gt#(s(x),0()) -> c_5()
10:W:quicksort#(nil()) -> c_8()
11:W:split#(pivot,nil()) -> c_11()
12:W:split'#(false(),x,pair(ls,rs)) -> c_12()
13:W:split'#(true(),x,pair(ls,rs)) -> c_13()
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
10: quicksort#(nil()) -> c_8()
11: split#(pivot,nil()) -> c_11()
12: split'#(false(),x,pair(ls,rs)) -> c_12()
13: split'#(true(),x,pair(ls,rs)) -> c_13()
7: gt#(0(),0()) -> c_3()
8: gt#(0(),s(y)) -> c_4()
9: gt#(s(x),0()) -> c_5()
6: append#(nil(),ys) -> c_2()
* Step 4: SimplifyRHS WORST_CASE(?,O(n^3))
+ Considered Problem:
- Strict DPs:
append#(dd(x,xs),ys) -> c_1(append#(xs,ys))
gt#(s(x),s(y)) -> c_6(gt#(x,y))
quicksort#(dd(z,zs)) -> c_7(quicksort'#(z,split(z,zs)),split#(z,zs))
quicksort'#(z,pair(xs,ys)) -> c_9(append#(quicksort(xs),dd(z,quicksort(ys))),quicksort#(xs),quicksort#(ys))
split#(pivot,dd(x,xs)) -> c_10(split'#(gt(x,pivot),x,split(pivot,xs)),gt#(x,pivot),split#(pivot,xs))
- Weak TRS:
append(dd(x,xs),ys) -> dd(x,append(xs,ys))
append(nil(),ys) -> ys
gt(0(),0()) -> false()
gt(0(),s(y)) -> false()
gt(s(x),0()) -> true()
gt(s(x),s(y)) -> gt(x,y)
quicksort(dd(z,zs)) -> quicksort'(z,split(z,zs))
quicksort(nil()) -> nil()
quicksort'(z,pair(xs,ys)) -> append(quicksort(xs),dd(z,quicksort(ys)))
split(pivot,dd(x,xs)) -> split'(gt(x,pivot),x,split(pivot,xs))
split(pivot,nil()) -> pair(nil(),nil())
split'(false(),x,pair(ls,rs)) -> pair(dd(x,ls),rs)
split'(true(),x,pair(ls,rs)) -> pair(ls,dd(x,rs))
- Signature:
{append/2,gt/2,quicksort/1,quicksort'/2,split/2,split'/3,append#/2,gt#/2,quicksort#/1,quicksort'#/2,split#/2
,split'#/3} / {0/0,dd/2,false/0,nil/0,pair/2,s/1,true/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/2,c_8/0
,c_9/3,c_10/3,c_11/0,c_12/0,c_13/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {append#,gt#,quicksort#,quicksort'#,split#
,split'#} and constructors {0,dd,false,nil,pair,s,true}
+ Applied Processor:
SimplifyRHS
+ Details:
Consider the dependency graph
1:S:append#(dd(x,xs),ys) -> c_1(append#(xs,ys))
-->_1 append#(dd(x,xs),ys) -> c_1(append#(xs,ys)):1
2:S:gt#(s(x),s(y)) -> c_6(gt#(x,y))
-->_1 gt#(s(x),s(y)) -> c_6(gt#(x,y)):2
3:S:quicksort#(dd(z,zs)) -> c_7(quicksort'#(z,split(z,zs)),split#(z,zs))
-->_2 split#(pivot,dd(x,xs)) -> c_10(split'#(gt(x,pivot),x,split(pivot,xs))
,gt#(x,pivot)
,split#(pivot,xs)):5
-->_1 quicksort'#(z,pair(xs,ys)) -> c_9(append#(quicksort(xs),dd(z,quicksort(ys)))
,quicksort#(xs)
,quicksort#(ys)):4
4:S:quicksort'#(z,pair(xs,ys)) -> c_9(append#(quicksort(xs),dd(z,quicksort(ys)))
,quicksort#(xs)
,quicksort#(ys))
-->_3 quicksort#(dd(z,zs)) -> c_7(quicksort'#(z,split(z,zs)),split#(z,zs)):3
-->_2 quicksort#(dd(z,zs)) -> c_7(quicksort'#(z,split(z,zs)),split#(z,zs)):3
-->_1 append#(dd(x,xs),ys) -> c_1(append#(xs,ys)):1
5:S:split#(pivot,dd(x,xs)) -> c_10(split'#(gt(x,pivot),x,split(pivot,xs)),gt#(x,pivot),split#(pivot,xs))
-->_3 split#(pivot,dd(x,xs)) -> c_10(split'#(gt(x,pivot),x,split(pivot,xs))
,gt#(x,pivot)
,split#(pivot,xs)):5
-->_2 gt#(s(x),s(y)) -> c_6(gt#(x,y)):2
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
split#(pivot,dd(x,xs)) -> c_10(gt#(x,pivot),split#(pivot,xs))
* Step 5: DecomposeDG WORST_CASE(?,O(n^3))
+ Considered Problem:
- Strict DPs:
append#(dd(x,xs),ys) -> c_1(append#(xs,ys))
gt#(s(x),s(y)) -> c_6(gt#(x,y))
quicksort#(dd(z,zs)) -> c_7(quicksort'#(z,split(z,zs)),split#(z,zs))
quicksort'#(z,pair(xs,ys)) -> c_9(append#(quicksort(xs),dd(z,quicksort(ys))),quicksort#(xs),quicksort#(ys))
split#(pivot,dd(x,xs)) -> c_10(gt#(x,pivot),split#(pivot,xs))
- Weak TRS:
append(dd(x,xs),ys) -> dd(x,append(xs,ys))
append(nil(),ys) -> ys
gt(0(),0()) -> false()
gt(0(),s(y)) -> false()
gt(s(x),0()) -> true()
gt(s(x),s(y)) -> gt(x,y)
quicksort(dd(z,zs)) -> quicksort'(z,split(z,zs))
quicksort(nil()) -> nil()
quicksort'(z,pair(xs,ys)) -> append(quicksort(xs),dd(z,quicksort(ys)))
split(pivot,dd(x,xs)) -> split'(gt(x,pivot),x,split(pivot,xs))
split(pivot,nil()) -> pair(nil(),nil())
split'(false(),x,pair(ls,rs)) -> pair(dd(x,ls),rs)
split'(true(),x,pair(ls,rs)) -> pair(ls,dd(x,rs))
- Signature:
{append/2,gt/2,quicksort/1,quicksort'/2,split/2,split'/3,append#/2,gt#/2,quicksort#/1,quicksort'#/2,split#/2
,split'#/3} / {0/0,dd/2,false/0,nil/0,pair/2,s/1,true/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/2,c_8/0
,c_9/3,c_10/2,c_11/0,c_12/0,c_13/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {append#,gt#,quicksort#,quicksort'#,split#
,split'#} and constructors {0,dd,false,nil,pair,s,true}
+ Applied Processor:
DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing}
+ Details:
We decompose the input problem according to the dependency graph into the upper component
quicksort#(dd(z,zs)) -> c_7(quicksort'#(z,split(z,zs)),split#(z,zs))
quicksort'#(z,pair(xs,ys)) -> c_9(append#(quicksort(xs),dd(z,quicksort(ys))),quicksort#(xs),quicksort#(ys))
and a lower component
append#(dd(x,xs),ys) -> c_1(append#(xs,ys))
gt#(s(x),s(y)) -> c_6(gt#(x,y))
split#(pivot,dd(x,xs)) -> c_10(gt#(x,pivot),split#(pivot,xs))
Further, following extension rules are added to the lower component.
quicksort#(dd(z,zs)) -> quicksort'#(z,split(z,zs))
quicksort#(dd(z,zs)) -> split#(z,zs)
quicksort'#(z,pair(xs,ys)) -> append#(quicksort(xs),dd(z,quicksort(ys)))
quicksort'#(z,pair(xs,ys)) -> quicksort#(xs)
quicksort'#(z,pair(xs,ys)) -> quicksort#(ys)
** Step 5.a:1: SimplifyRHS WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
quicksort#(dd(z,zs)) -> c_7(quicksort'#(z,split(z,zs)),split#(z,zs))
quicksort'#(z,pair(xs,ys)) -> c_9(append#(quicksort(xs),dd(z,quicksort(ys))),quicksort#(xs),quicksort#(ys))
- Weak TRS:
append(dd(x,xs),ys) -> dd(x,append(xs,ys))
append(nil(),ys) -> ys
gt(0(),0()) -> false()
gt(0(),s(y)) -> false()
gt(s(x),0()) -> true()
gt(s(x),s(y)) -> gt(x,y)
quicksort(dd(z,zs)) -> quicksort'(z,split(z,zs))
quicksort(nil()) -> nil()
quicksort'(z,pair(xs,ys)) -> append(quicksort(xs),dd(z,quicksort(ys)))
split(pivot,dd(x,xs)) -> split'(gt(x,pivot),x,split(pivot,xs))
split(pivot,nil()) -> pair(nil(),nil())
split'(false(),x,pair(ls,rs)) -> pair(dd(x,ls),rs)
split'(true(),x,pair(ls,rs)) -> pair(ls,dd(x,rs))
- Signature:
{append/2,gt/2,quicksort/1,quicksort'/2,split/2,split'/3,append#/2,gt#/2,quicksort#/1,quicksort'#/2,split#/2
,split'#/3} / {0/0,dd/2,false/0,nil/0,pair/2,s/1,true/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/2,c_8/0
,c_9/3,c_10/2,c_11/0,c_12/0,c_13/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {append#,gt#,quicksort#,quicksort'#,split#
,split'#} and constructors {0,dd,false,nil,pair,s,true}
+ Applied Processor:
SimplifyRHS
+ Details:
Consider the dependency graph
1:S:quicksort#(dd(z,zs)) -> c_7(quicksort'#(z,split(z,zs)),split#(z,zs))
-->_1 quicksort'#(z,pair(xs,ys)) -> c_9(append#(quicksort(xs),dd(z,quicksort(ys)))
,quicksort#(xs)
,quicksort#(ys)):2
2:S:quicksort'#(z,pair(xs,ys)) -> c_9(append#(quicksort(xs),dd(z,quicksort(ys)))
,quicksort#(xs)
,quicksort#(ys))
-->_3 quicksort#(dd(z,zs)) -> c_7(quicksort'#(z,split(z,zs)),split#(z,zs)):1
-->_2 quicksort#(dd(z,zs)) -> c_7(quicksort'#(z,split(z,zs)),split#(z,zs)):1
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
quicksort#(dd(z,zs)) -> c_7(quicksort'#(z,split(z,zs)))
quicksort'#(z,pair(xs,ys)) -> c_9(quicksort#(xs),quicksort#(ys))
** Step 5.a:2: UsableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
quicksort#(dd(z,zs)) -> c_7(quicksort'#(z,split(z,zs)))
quicksort'#(z,pair(xs,ys)) -> c_9(quicksort#(xs),quicksort#(ys))
- Weak TRS:
append(dd(x,xs),ys) -> dd(x,append(xs,ys))
append(nil(),ys) -> ys
gt(0(),0()) -> false()
gt(0(),s(y)) -> false()
gt(s(x),0()) -> true()
gt(s(x),s(y)) -> gt(x,y)
quicksort(dd(z,zs)) -> quicksort'(z,split(z,zs))
quicksort(nil()) -> nil()
quicksort'(z,pair(xs,ys)) -> append(quicksort(xs),dd(z,quicksort(ys)))
split(pivot,dd(x,xs)) -> split'(gt(x,pivot),x,split(pivot,xs))
split(pivot,nil()) -> pair(nil(),nil())
split'(false(),x,pair(ls,rs)) -> pair(dd(x,ls),rs)
split'(true(),x,pair(ls,rs)) -> pair(ls,dd(x,rs))
- Signature:
{append/2,gt/2,quicksort/1,quicksort'/2,split/2,split'/3,append#/2,gt#/2,quicksort#/1,quicksort'#/2,split#/2
,split'#/3} / {0/0,dd/2,false/0,nil/0,pair/2,s/1,true/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/1,c_8/0
,c_9/2,c_10/2,c_11/0,c_12/0,c_13/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {append#,gt#,quicksort#,quicksort'#,split#
,split'#} and constructors {0,dd,false,nil,pair,s,true}
+ Applied Processor:
UsableRules
+ Details:
We replace rewrite rules by usable rules:
gt(0(),0()) -> false()
gt(0(),s(y)) -> false()
gt(s(x),0()) -> true()
gt(s(x),s(y)) -> gt(x,y)
split(pivot,dd(x,xs)) -> split'(gt(x,pivot),x,split(pivot,xs))
split(pivot,nil()) -> pair(nil(),nil())
split'(false(),x,pair(ls,rs)) -> pair(dd(x,ls),rs)
split'(true(),x,pair(ls,rs)) -> pair(ls,dd(x,rs))
quicksort#(dd(z,zs)) -> c_7(quicksort'#(z,split(z,zs)))
quicksort'#(z,pair(xs,ys)) -> c_9(quicksort#(xs),quicksort#(ys))
** Step 5.a:3: Ara WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
quicksort#(dd(z,zs)) -> c_7(quicksort'#(z,split(z,zs)))
quicksort'#(z,pair(xs,ys)) -> c_9(quicksort#(xs),quicksort#(ys))
- Weak TRS:
gt(0(),0()) -> false()
gt(0(),s(y)) -> false()
gt(s(x),0()) -> true()
gt(s(x),s(y)) -> gt(x,y)
split(pivot,dd(x,xs)) -> split'(gt(x,pivot),x,split(pivot,xs))
split(pivot,nil()) -> pair(nil(),nil())
split'(false(),x,pair(ls,rs)) -> pair(dd(x,ls),rs)
split'(true(),x,pair(ls,rs)) -> pair(ls,dd(x,rs))
- Signature:
{append/2,gt/2,quicksort/1,quicksort'/2,split/2,split'/3,append#/2,gt#/2,quicksort#/1,quicksort'#/2,split#/2
,split'#/3} / {0/0,dd/2,false/0,nil/0,pair/2,s/1,true/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/1,c_8/0
,c_9/2,c_10/2,c_11/0,c_12/0,c_13/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {append#,gt#,quicksort#,quicksort'#,split#
,split'#} and constructors {0,dd,false,nil,pair,s,true}
+ Applied Processor:
Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1}
+ Details:
Signatures used:
----------------
0 :: [] -(0)-> "A"(0)
dd :: ["A"(0) x "A"(2)] -(2)-> "A"(2)
false :: [] -(0)-> "A"(0)
false :: [] -(0)-> "A"(15)
gt :: ["A"(0) x "A"(0)] -(0)-> "A"(9)
nil :: [] -(0)-> "A"(2)
nil :: [] -(0)-> "A"(15)
pair :: ["A"(2) x "A"(2)] -(0)-> "A"(2)
pair :: ["A"(15) x "A"(15)] -(0)-> "A"(15)
s :: ["A"(0)] -(0)-> "A"(0)
split :: ["A"(0) x "A"(2)] -(0)-> "A"(2)
split' :: ["A"(0) x "A"(0) x "A"(2)] -(2)-> "A"(2)
true :: [] -(0)-> "A"(0)
true :: [] -(0)-> "A"(15)
quicksort# :: ["A"(2)] -(0)-> "A"(4)
quicksort'# :: ["A"(0) x "A"(2)] -(1)-> "A"(13)
c_7 :: ["A"(0)] -(0)-> "A"(12)
c_9 :: ["A"(0) x "A"(0)] -(0)-> "A"(15)
Cost-free Signatures used:
--------------------------
Base Constructor Signatures used:
---------------------------------
"0_A" :: [] -(0)-> "A"(1)
"c_7_A" :: ["A"(0)] -(0)-> "A"(1)
"c_9_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1)
"dd_A" :: ["A"(0) x "A"(1)] -(1)-> "A"(1)
"false_A" :: [] -(0)-> "A"(1)
"nil_A" :: [] -(0)-> "A"(1)
"pair_A" :: ["A"(1) x "A"(1)] -(0)-> "A"(1)
"s_A" :: ["A"(1)] -(1)-> "A"(1)
"true_A" :: [] -(0)-> "A"(1)
Following Still Strict Rules were Typed as:
-------------------------------------------
1. Strict:
quicksort#(dd(z,zs)) -> c_7(quicksort'#(z,split(z,zs)))
quicksort'#(z,pair(xs,ys)) -> c_9(quicksort#(xs),quicksort#(ys))
2. Weak:
** Step 5.b:1: DecomposeDG WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
append#(dd(x,xs),ys) -> c_1(append#(xs,ys))
gt#(s(x),s(y)) -> c_6(gt#(x,y))
split#(pivot,dd(x,xs)) -> c_10(gt#(x,pivot),split#(pivot,xs))
- Weak DPs:
quicksort#(dd(z,zs)) -> quicksort'#(z,split(z,zs))
quicksort#(dd(z,zs)) -> split#(z,zs)
quicksort'#(z,pair(xs,ys)) -> append#(quicksort(xs),dd(z,quicksort(ys)))
quicksort'#(z,pair(xs,ys)) -> quicksort#(xs)
quicksort'#(z,pair(xs,ys)) -> quicksort#(ys)
- Weak TRS:
append(dd(x,xs),ys) -> dd(x,append(xs,ys))
append(nil(),ys) -> ys
gt(0(),0()) -> false()
gt(0(),s(y)) -> false()
gt(s(x),0()) -> true()
gt(s(x),s(y)) -> gt(x,y)
quicksort(dd(z,zs)) -> quicksort'(z,split(z,zs))
quicksort(nil()) -> nil()
quicksort'(z,pair(xs,ys)) -> append(quicksort(xs),dd(z,quicksort(ys)))
split(pivot,dd(x,xs)) -> split'(gt(x,pivot),x,split(pivot,xs))
split(pivot,nil()) -> pair(nil(),nil())
split'(false(),x,pair(ls,rs)) -> pair(dd(x,ls),rs)
split'(true(),x,pair(ls,rs)) -> pair(ls,dd(x,rs))
- Signature:
{append/2,gt/2,quicksort/1,quicksort'/2,split/2,split'/3,append#/2,gt#/2,quicksort#/1,quicksort'#/2,split#/2
,split'#/3} / {0/0,dd/2,false/0,nil/0,pair/2,s/1,true/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/2,c_8/0
,c_9/3,c_10/2,c_11/0,c_12/0,c_13/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {append#,gt#,quicksort#,quicksort'#,split#
,split'#} and constructors {0,dd,false,nil,pair,s,true}
+ Applied Processor:
DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing}
+ Details:
We decompose the input problem according to the dependency graph into the upper component
append#(dd(x,xs),ys) -> c_1(append#(xs,ys))
quicksort#(dd(z,zs)) -> quicksort'#(z,split(z,zs))
quicksort#(dd(z,zs)) -> split#(z,zs)
quicksort'#(z,pair(xs,ys)) -> append#(quicksort(xs),dd(z,quicksort(ys)))
quicksort'#(z,pair(xs,ys)) -> quicksort#(xs)
quicksort'#(z,pair(xs,ys)) -> quicksort#(ys)
split#(pivot,dd(x,xs)) -> c_10(gt#(x,pivot),split#(pivot,xs))
and a lower component
gt#(s(x),s(y)) -> c_6(gt#(x,y))
Further, following extension rules are added to the lower component.
append#(dd(x,xs),ys) -> append#(xs,ys)
quicksort#(dd(z,zs)) -> quicksort'#(z,split(z,zs))
quicksort#(dd(z,zs)) -> split#(z,zs)
quicksort'#(z,pair(xs,ys)) -> append#(quicksort(xs),dd(z,quicksort(ys)))
quicksort'#(z,pair(xs,ys)) -> quicksort#(xs)
quicksort'#(z,pair(xs,ys)) -> quicksort#(ys)
split#(pivot,dd(x,xs)) -> gt#(x,pivot)
split#(pivot,dd(x,xs)) -> split#(pivot,xs)
*** Step 5.b:1.a:1: SimplifyRHS WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
append#(dd(x,xs),ys) -> c_1(append#(xs,ys))
split#(pivot,dd(x,xs)) -> c_10(gt#(x,pivot),split#(pivot,xs))
- Weak DPs:
quicksort#(dd(z,zs)) -> quicksort'#(z,split(z,zs))
quicksort#(dd(z,zs)) -> split#(z,zs)
quicksort'#(z,pair(xs,ys)) -> append#(quicksort(xs),dd(z,quicksort(ys)))
quicksort'#(z,pair(xs,ys)) -> quicksort#(xs)
quicksort'#(z,pair(xs,ys)) -> quicksort#(ys)
- Weak TRS:
append(dd(x,xs),ys) -> dd(x,append(xs,ys))
append(nil(),ys) -> ys
gt(0(),0()) -> false()
gt(0(),s(y)) -> false()
gt(s(x),0()) -> true()
gt(s(x),s(y)) -> gt(x,y)
quicksort(dd(z,zs)) -> quicksort'(z,split(z,zs))
quicksort(nil()) -> nil()
quicksort'(z,pair(xs,ys)) -> append(quicksort(xs),dd(z,quicksort(ys)))
split(pivot,dd(x,xs)) -> split'(gt(x,pivot),x,split(pivot,xs))
split(pivot,nil()) -> pair(nil(),nil())
split'(false(),x,pair(ls,rs)) -> pair(dd(x,ls),rs)
split'(true(),x,pair(ls,rs)) -> pair(ls,dd(x,rs))
- Signature:
{append/2,gt/2,quicksort/1,quicksort'/2,split/2,split'/3,append#/2,gt#/2,quicksort#/1,quicksort'#/2,split#/2
,split'#/3} / {0/0,dd/2,false/0,nil/0,pair/2,s/1,true/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/2,c_8/0
,c_9/3,c_10/2,c_11/0,c_12/0,c_13/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {append#,gt#,quicksort#,quicksort'#,split#
,split'#} and constructors {0,dd,false,nil,pair,s,true}
+ Applied Processor:
SimplifyRHS
+ Details:
Consider the dependency graph
1:S:append#(dd(x,xs),ys) -> c_1(append#(xs,ys))
-->_1 append#(dd(x,xs),ys) -> c_1(append#(xs,ys)):1
2:S:split#(pivot,dd(x,xs)) -> c_10(gt#(x,pivot),split#(pivot,xs))
-->_2 split#(pivot,dd(x,xs)) -> c_10(gt#(x,pivot),split#(pivot,xs)):2
3:W:quicksort#(dd(z,zs)) -> quicksort'#(z,split(z,zs))
-->_1 quicksort'#(z,pair(xs,ys)) -> quicksort#(ys):7
-->_1 quicksort'#(z,pair(xs,ys)) -> quicksort#(xs):6
-->_1 quicksort'#(z,pair(xs,ys)) -> append#(quicksort(xs),dd(z,quicksort(ys))):5
4:W:quicksort#(dd(z,zs)) -> split#(z,zs)
-->_1 split#(pivot,dd(x,xs)) -> c_10(gt#(x,pivot),split#(pivot,xs)):2
5:W:quicksort'#(z,pair(xs,ys)) -> append#(quicksort(xs),dd(z,quicksort(ys)))
-->_1 append#(dd(x,xs),ys) -> c_1(append#(xs,ys)):1
6:W:quicksort'#(z,pair(xs,ys)) -> quicksort#(xs)
-->_1 quicksort#(dd(z,zs)) -> split#(z,zs):4
-->_1 quicksort#(dd(z,zs)) -> quicksort'#(z,split(z,zs)):3
7:W:quicksort'#(z,pair(xs,ys)) -> quicksort#(ys)
-->_1 quicksort#(dd(z,zs)) -> split#(z,zs):4
-->_1 quicksort#(dd(z,zs)) -> quicksort'#(z,split(z,zs)):3
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
split#(pivot,dd(x,xs)) -> c_10(split#(pivot,xs))
*** Step 5.b:1.a:2: Ara WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
append#(dd(x,xs),ys) -> c_1(append#(xs,ys))
split#(pivot,dd(x,xs)) -> c_10(split#(pivot,xs))
- Weak DPs:
quicksort#(dd(z,zs)) -> quicksort'#(z,split(z,zs))
quicksort#(dd(z,zs)) -> split#(z,zs)
quicksort'#(z,pair(xs,ys)) -> append#(quicksort(xs),dd(z,quicksort(ys)))
quicksort'#(z,pair(xs,ys)) -> quicksort#(xs)
quicksort'#(z,pair(xs,ys)) -> quicksort#(ys)
- Weak TRS:
append(dd(x,xs),ys) -> dd(x,append(xs,ys))
append(nil(),ys) -> ys
gt(0(),0()) -> false()
gt(0(),s(y)) -> false()
gt(s(x),0()) -> true()
gt(s(x),s(y)) -> gt(x,y)
quicksort(dd(z,zs)) -> quicksort'(z,split(z,zs))
quicksort(nil()) -> nil()
quicksort'(z,pair(xs,ys)) -> append(quicksort(xs),dd(z,quicksort(ys)))
split(pivot,dd(x,xs)) -> split'(gt(x,pivot),x,split(pivot,xs))
split(pivot,nil()) -> pair(nil(),nil())
split'(false(),x,pair(ls,rs)) -> pair(dd(x,ls),rs)
split'(true(),x,pair(ls,rs)) -> pair(ls,dd(x,rs))
- Signature:
{append/2,gt/2,quicksort/1,quicksort'/2,split/2,split'/3,append#/2,gt#/2,quicksort#/1,quicksort'#/2,split#/2
,split'#/3} / {0/0,dd/2,false/0,nil/0,pair/2,s/1,true/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/2,c_8/0
,c_9/3,c_10/1,c_11/0,c_12/0,c_13/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {append#,gt#,quicksort#,quicksort'#,split#
,split'#} and constructors {0,dd,false,nil,pair,s,true}
+ Applied Processor:
Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1}
+ Details:
Signatures used:
----------------
0 :: [] -(0)-> "A"(0)
append :: ["A"(5) x "A"(5)] -(9)-> "A"(5)
dd :: ["A"(0) x "A"(0)] -(0)-> "A"(0)
dd :: ["A"(0) x "A"(15)] -(15)-> "A"(15)
dd :: ["A"(0) x "A"(5)] -(5)-> "A"(5)
dd :: ["A"(0) x "A"(1)] -(1)-> "A"(1)
false :: [] -(0)-> "A"(0)
false :: [] -(0)-> "A"(15)
gt :: ["A"(0) x "A"(0)] -(0)-> "A"(9)
nil :: [] -(0)-> "A"(5)
nil :: [] -(0)-> "A"(15)
nil :: [] -(0)-> "A"(11)
pair :: ["A"(15) x "A"(15)] -(0)-> "A"(15)
quicksort :: ["A"(15)] -(0)-> "A"(5)
quicksort' :: ["A"(0) x "A"(15)] -(15)-> "A"(5)
s :: ["A"(0)] -(0)-> "A"(0)
split :: ["A"(0) x "A"(15)] -(0)-> "A"(15)
split' :: ["A"(0) x "A"(0) x "A"(15)] -(15)-> "A"(15)
true :: [] -(0)-> "A"(0)
true :: [] -(0)-> "A"(15)
append# :: ["A"(0) x "A"(0)] -(0)-> "A"(1)
quicksort# :: ["A"(15)] -(2)-> "A"(1)
quicksort'# :: ["A"(0) x "A"(15)] -(6)-> "A"(1)
split# :: ["A"(0) x "A"(15)] -(8)-> "A"(1)
c_1 :: ["A"(0)] -(0)-> "A"(12)
c_10 :: ["A"(0)] -(0)-> "A"(12)
Cost-free Signatures used:
--------------------------
Base Constructor Signatures used:
---------------------------------
"0_A" :: [] -(0)-> "A"(1)
"c_10_A" :: ["A"(0)] -(0)-> "A"(1)
"c_1_A" :: ["A"(0)] -(0)-> "A"(1)
"dd_A" :: ["A"(0) x "A"(1)] -(1)-> "A"(1)
"false_A" :: [] -(0)-> "A"(1)
"nil_A" :: [] -(0)-> "A"(1)
"pair_A" :: ["A"(1) x "A"(1)] -(0)-> "A"(1)
"s_A" :: ["A"(0)] -(0)-> "A"(1)
"true_A" :: [] -(0)-> "A"(1)
Following Still Strict Rules were Typed as:
-------------------------------------------
1. Strict:
split#(pivot,dd(x,xs)) -> c_10(split#(pivot,xs))
2. Weak:
append#(dd(x,xs),ys) -> c_1(append#(xs,ys))
*** Step 5.b:1.a:3: Ara WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
append#(dd(x,xs),ys) -> c_1(append#(xs,ys))
- Weak DPs:
quicksort#(dd(z,zs)) -> quicksort'#(z,split(z,zs))
quicksort#(dd(z,zs)) -> split#(z,zs)
quicksort'#(z,pair(xs,ys)) -> append#(quicksort(xs),dd(z,quicksort(ys)))
quicksort'#(z,pair(xs,ys)) -> quicksort#(xs)
quicksort'#(z,pair(xs,ys)) -> quicksort#(ys)
split#(pivot,dd(x,xs)) -> c_10(split#(pivot,xs))
- Weak TRS:
append(dd(x,xs),ys) -> dd(x,append(xs,ys))
append(nil(),ys) -> ys
gt(0(),0()) -> false()
gt(0(),s(y)) -> false()
gt(s(x),0()) -> true()
gt(s(x),s(y)) -> gt(x,y)
quicksort(dd(z,zs)) -> quicksort'(z,split(z,zs))
quicksort(nil()) -> nil()
quicksort'(z,pair(xs,ys)) -> append(quicksort(xs),dd(z,quicksort(ys)))
split(pivot,dd(x,xs)) -> split'(gt(x,pivot),x,split(pivot,xs))
split(pivot,nil()) -> pair(nil(),nil())
split'(false(),x,pair(ls,rs)) -> pair(dd(x,ls),rs)
split'(true(),x,pair(ls,rs)) -> pair(ls,dd(x,rs))
- Signature:
{append/2,gt/2,quicksort/1,quicksort'/2,split/2,split'/3,append#/2,gt#/2,quicksort#/1,quicksort'#/2,split#/2
,split'#/3} / {0/0,dd/2,false/0,nil/0,pair/2,s/1,true/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/2,c_8/0
,c_9/3,c_10/1,c_11/0,c_12/0,c_13/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {append#,gt#,quicksort#,quicksort'#,split#
,split'#} and constructors {0,dd,false,nil,pair,s,true}
+ Applied Processor:
Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1}
+ Details:
Signatures used:
----------------
0 :: [] -(0)-> "A"(0)
append :: ["A"(1) x "A"(1)] -(0)-> "A"(1)
dd :: ["A"(0) x "A"(1)] -(1)-> "A"(1)
dd :: ["A"(0) x "A"(8)] -(8)-> "A"(8)
dd :: ["A"(0) x "A"(7)] -(7)-> "A"(7)
dd :: ["A"(0) x "A"(0)] -(0)-> "A"(0)
false :: [] -(0)-> "A"(0)
false :: [] -(0)-> "A"(15)
gt :: ["A"(0) x "A"(0)] -(0)-> "A"(9)
nil :: [] -(0)-> "A"(1)
nil :: [] -(0)-> "A"(8)
nil :: [] -(0)-> "A"(7)
nil :: [] -(0)-> "A"(15)
pair :: ["A"(8) x "A"(8)] -(0)-> "A"(8)
pair :: ["A"(10) x "A"(10)] -(0)-> "A"(10)
quicksort :: ["A"(8)] -(0)-> "A"(1)
quicksort' :: ["A"(0) x "A"(8)] -(4)-> "A"(1)
s :: ["A"(0)] -(0)-> "A"(0)
split :: ["A"(0) x "A"(8)] -(0)-> "A"(8)
split' :: ["A"(0) x "A"(0) x "A"(8)] -(8)-> "A"(8)
true :: [] -(0)-> "A"(0)
true :: [] -(0)-> "A"(15)
append# :: ["A"(1) x "A"(0)] -(0)-> "A"(1)
quicksort# :: ["A"(8)] -(9)-> "A"(1)
quicksort'# :: ["A"(0) x "A"(8)] -(13)-> "A"(1)
split# :: ["A"(0) x "A"(7)] -(9)-> "A"(12)
c_1 :: ["A"(0)] -(0)-> "A"(12)
c_10 :: ["A"(0)] -(0)-> "A"(15)
Cost-free Signatures used:
--------------------------
Base Constructor Signatures used:
---------------------------------
"0_A" :: [] -(0)-> "A"(1)
"c_10_A" :: ["A"(0)] -(0)-> "A"(1)
"c_1_A" :: ["A"(0)] -(0)-> "A"(1)
"dd_A" :: ["A"(0) x "A"(1)] -(1)-> "A"(1)
"false_A" :: [] -(0)-> "A"(1)
"nil_A" :: [] -(0)-> "A"(1)
"pair_A" :: ["A"(1) x "A"(1)] -(0)-> "A"(1)
"s_A" :: ["A"(0)] -(0)-> "A"(1)
"true_A" :: [] -(0)-> "A"(1)
Following Still Strict Rules were Typed as:
-------------------------------------------
1. Strict:
append#(dd(x,xs),ys) -> c_1(append#(xs,ys))
2. Weak:
*** Step 5.b:1.b:1: RemoveWeakSuffixes WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
gt#(s(x),s(y)) -> c_6(gt#(x,y))
- Weak DPs:
append#(dd(x,xs),ys) -> append#(xs,ys)
quicksort#(dd(z,zs)) -> quicksort'#(z,split(z,zs))
quicksort#(dd(z,zs)) -> split#(z,zs)
quicksort'#(z,pair(xs,ys)) -> append#(quicksort(xs),dd(z,quicksort(ys)))
quicksort'#(z,pair(xs,ys)) -> quicksort#(xs)
quicksort'#(z,pair(xs,ys)) -> quicksort#(ys)
split#(pivot,dd(x,xs)) -> gt#(x,pivot)
split#(pivot,dd(x,xs)) -> split#(pivot,xs)
- Weak TRS:
append(dd(x,xs),ys) -> dd(x,append(xs,ys))
append(nil(),ys) -> ys
gt(0(),0()) -> false()
gt(0(),s(y)) -> false()
gt(s(x),0()) -> true()
gt(s(x),s(y)) -> gt(x,y)
quicksort(dd(z,zs)) -> quicksort'(z,split(z,zs))
quicksort(nil()) -> nil()
quicksort'(z,pair(xs,ys)) -> append(quicksort(xs),dd(z,quicksort(ys)))
split(pivot,dd(x,xs)) -> split'(gt(x,pivot),x,split(pivot,xs))
split(pivot,nil()) -> pair(nil(),nil())
split'(false(),x,pair(ls,rs)) -> pair(dd(x,ls),rs)
split'(true(),x,pair(ls,rs)) -> pair(ls,dd(x,rs))
- Signature:
{append/2,gt/2,quicksort/1,quicksort'/2,split/2,split'/3,append#/2,gt#/2,quicksort#/1,quicksort'#/2,split#/2
,split'#/3} / {0/0,dd/2,false/0,nil/0,pair/2,s/1,true/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/2,c_8/0
,c_9/3,c_10/2,c_11/0,c_12/0,c_13/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {append#,gt#,quicksort#,quicksort'#,split#
,split'#} and constructors {0,dd,false,nil,pair,s,true}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:S:gt#(s(x),s(y)) -> c_6(gt#(x,y))
-->_1 gt#(s(x),s(y)) -> c_6(gt#(x,y)):1
2:W:append#(dd(x,xs),ys) -> append#(xs,ys)
-->_1 append#(dd(x,xs),ys) -> append#(xs,ys):2
3:W:quicksort#(dd(z,zs)) -> quicksort'#(z,split(z,zs))
-->_1 quicksort'#(z,pair(xs,ys)) -> quicksort#(ys):7
-->_1 quicksort'#(z,pair(xs,ys)) -> quicksort#(xs):6
-->_1 quicksort'#(z,pair(xs,ys)) -> append#(quicksort(xs),dd(z,quicksort(ys))):5
4:W:quicksort#(dd(z,zs)) -> split#(z,zs)
-->_1 split#(pivot,dd(x,xs)) -> split#(pivot,xs):9
-->_1 split#(pivot,dd(x,xs)) -> gt#(x,pivot):8
5:W:quicksort'#(z,pair(xs,ys)) -> append#(quicksort(xs),dd(z,quicksort(ys)))
-->_1 append#(dd(x,xs),ys) -> append#(xs,ys):2
6:W:quicksort'#(z,pair(xs,ys)) -> quicksort#(xs)
-->_1 quicksort#(dd(z,zs)) -> split#(z,zs):4
-->_1 quicksort#(dd(z,zs)) -> quicksort'#(z,split(z,zs)):3
7:W:quicksort'#(z,pair(xs,ys)) -> quicksort#(ys)
-->_1 quicksort#(dd(z,zs)) -> split#(z,zs):4
-->_1 quicksort#(dd(z,zs)) -> quicksort'#(z,split(z,zs)):3
8:W:split#(pivot,dd(x,xs)) -> gt#(x,pivot)
-->_1 gt#(s(x),s(y)) -> c_6(gt#(x,y)):1
9:W:split#(pivot,dd(x,xs)) -> split#(pivot,xs)
-->_1 split#(pivot,dd(x,xs)) -> split#(pivot,xs):9
-->_1 split#(pivot,dd(x,xs)) -> gt#(x,pivot):8
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
5: quicksort'#(z,pair(xs,ys)) -> append#(quicksort(xs),dd(z,quicksort(ys)))
2: append#(dd(x,xs),ys) -> append#(xs,ys)
*** Step 5.b:1.b:2: UsableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
gt#(s(x),s(y)) -> c_6(gt#(x,y))
- Weak DPs:
quicksort#(dd(z,zs)) -> quicksort'#(z,split(z,zs))
quicksort#(dd(z,zs)) -> split#(z,zs)
quicksort'#(z,pair(xs,ys)) -> quicksort#(xs)
quicksort'#(z,pair(xs,ys)) -> quicksort#(ys)
split#(pivot,dd(x,xs)) -> gt#(x,pivot)
split#(pivot,dd(x,xs)) -> split#(pivot,xs)
- Weak TRS:
append(dd(x,xs),ys) -> dd(x,append(xs,ys))
append(nil(),ys) -> ys
gt(0(),0()) -> false()
gt(0(),s(y)) -> false()
gt(s(x),0()) -> true()
gt(s(x),s(y)) -> gt(x,y)
quicksort(dd(z,zs)) -> quicksort'(z,split(z,zs))
quicksort(nil()) -> nil()
quicksort'(z,pair(xs,ys)) -> append(quicksort(xs),dd(z,quicksort(ys)))
split(pivot,dd(x,xs)) -> split'(gt(x,pivot),x,split(pivot,xs))
split(pivot,nil()) -> pair(nil(),nil())
split'(false(),x,pair(ls,rs)) -> pair(dd(x,ls),rs)
split'(true(),x,pair(ls,rs)) -> pair(ls,dd(x,rs))
- Signature:
{append/2,gt/2,quicksort/1,quicksort'/2,split/2,split'/3,append#/2,gt#/2,quicksort#/1,quicksort'#/2,split#/2
,split'#/3} / {0/0,dd/2,false/0,nil/0,pair/2,s/1,true/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/2,c_8/0
,c_9/3,c_10/2,c_11/0,c_12/0,c_13/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {append#,gt#,quicksort#,quicksort'#,split#
,split'#} and constructors {0,dd,false,nil,pair,s,true}
+ Applied Processor:
UsableRules
+ Details:
We replace rewrite rules by usable rules:
gt(0(),0()) -> false()
gt(0(),s(y)) -> false()
gt(s(x),0()) -> true()
gt(s(x),s(y)) -> gt(x,y)
split(pivot,dd(x,xs)) -> split'(gt(x,pivot),x,split(pivot,xs))
split(pivot,nil()) -> pair(nil(),nil())
split'(false(),x,pair(ls,rs)) -> pair(dd(x,ls),rs)
split'(true(),x,pair(ls,rs)) -> pair(ls,dd(x,rs))
gt#(s(x),s(y)) -> c_6(gt#(x,y))
quicksort#(dd(z,zs)) -> quicksort'#(z,split(z,zs))
quicksort#(dd(z,zs)) -> split#(z,zs)
quicksort'#(z,pair(xs,ys)) -> quicksort#(xs)
quicksort'#(z,pair(xs,ys)) -> quicksort#(ys)
split#(pivot,dd(x,xs)) -> gt#(x,pivot)
split#(pivot,dd(x,xs)) -> split#(pivot,xs)
*** Step 5.b:1.b:3: Ara WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
gt#(s(x),s(y)) -> c_6(gt#(x,y))
- Weak DPs:
quicksort#(dd(z,zs)) -> quicksort'#(z,split(z,zs))
quicksort#(dd(z,zs)) -> split#(z,zs)
quicksort'#(z,pair(xs,ys)) -> quicksort#(xs)
quicksort'#(z,pair(xs,ys)) -> quicksort#(ys)
split#(pivot,dd(x,xs)) -> gt#(x,pivot)
split#(pivot,dd(x,xs)) -> split#(pivot,xs)
- Weak TRS:
gt(0(),0()) -> false()
gt(0(),s(y)) -> false()
gt(s(x),0()) -> true()
gt(s(x),s(y)) -> gt(x,y)
split(pivot,dd(x,xs)) -> split'(gt(x,pivot),x,split(pivot,xs))
split(pivot,nil()) -> pair(nil(),nil())
split'(false(),x,pair(ls,rs)) -> pair(dd(x,ls),rs)
split'(true(),x,pair(ls,rs)) -> pair(ls,dd(x,rs))
- Signature:
{append/2,gt/2,quicksort/1,quicksort'/2,split/2,split'/3,append#/2,gt#/2,quicksort#/1,quicksort'#/2,split#/2
,split'#/3} / {0/0,dd/2,false/0,nil/0,pair/2,s/1,true/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/2,c_8/0
,c_9/3,c_10/2,c_11/0,c_12/0,c_13/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {append#,gt#,quicksort#,quicksort'#,split#
,split'#} and constructors {0,dd,false,nil,pair,s,true}
+ Applied Processor:
Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1}
+ Details:
Signatures used:
----------------
0 :: [] -(0)-> "A"(0)
dd :: ["A"(6) x "A"(6)] -(6)-> "A"(6)
false :: [] -(0)-> "A"(0)
false :: [] -(0)-> "A"(14)
gt :: ["A"(0) x "A"(0)] -(0)-> "A"(0)
nil :: [] -(0)-> "A"(6)
nil :: [] -(0)-> "A"(14)
pair :: ["A"(6) x "A"(6)] -(0)-> "A"(6)
pair :: ["A"(14) x "A"(14)] -(0)-> "A"(14)
s :: ["A"(0)] -(0)-> "A"(0)
s :: ["A"(1)] -(1)-> "A"(1)
split :: ["A"(0) x "A"(6)] -(1)-> "A"(6)
split' :: ["A"(0) x "A"(6) x "A"(6)] -(6)-> "A"(6)
true :: [] -(0)-> "A"(0)
true :: [] -(0)-> "A"(14)
gt# :: ["A"(0) x "A"(1)] -(6)-> "A"(0)
quicksort# :: ["A"(6)] -(14)-> "A"(0)
quicksort'# :: ["A"(0) x "A"(6)] -(15)-> "A"(0)
split# :: ["A"(5) x "A"(6)] -(5)-> "A"(0)
c_6 :: ["A"(0)] -(0)-> "A"(14)
Cost-free Signatures used:
--------------------------
Base Constructor Signatures used:
---------------------------------
"0_A" :: [] -(0)-> "A"(1)
"c_6_A" :: ["A"(0)] -(0)-> "A"(1)
"dd_A" :: ["A"(1) x "A"(1)] -(1)-> "A"(1)
"false_A" :: [] -(0)-> "A"(1)
"nil_A" :: [] -(0)-> "A"(1)
"pair_A" :: ["A"(1) x "A"(1)] -(0)-> "A"(1)
"s_A" :: ["A"(1)] -(1)-> "A"(1)
"true_A" :: [] -(0)-> "A"(1)
Following Still Strict Rules were Typed as:
-------------------------------------------
1. Strict:
gt#(s(x),s(y)) -> c_6(gt#(x,y))
2. Weak:
WORST_CASE(?,O(n^3))